Nuprl Lemma : reduce_wf
11,40
postcript
pdf
A
,
B
:Type,
f
:(
A
B
B
),
k
:
B
,
as
:(
A
List). reduce(
f
;
k
;
as
)
B
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
Y
,
reduce(
f
;
k
;
as
)
origin
A,B:Type, f:(A
BB), k:B, as:(A List). reduce(f; k; as) 
B A,B:Type, f:(ABB), k:B, as:(A List). reduce(f; k; as) B Tx:A. B(x)